\begin{tabbing}
$\forall$$T$:Type, $P$,$Q$:(($T$ List)$\rightarrow$prop\{i:l\}), $L$:($T$ List).
\\[0ex](star{-}append($T$; $P$; $Q$)($L$))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(($Q$($L$))\+
\\[0ex]$\vee$ ($\exists$$L_{1}$,$L_{2}$:$T$ List. (($L$ = append($L_{1}$; $L_{2}$)) $\wedge$ ($P$($L_{1}$)) $\wedge$ (star{-}append($T$; $P$; $Q$)($L_{2}$)))))
\-
\end{tabbing}